es:ES, A:Type, X:AbsInterface(A).
X is finite
 (locs:Id List
 (knds:Id(Knd List)
 ((e:E. ((e  X))  ((loc(e)  locs) & (kind(e)  knds(loc(e)))))) 

latex

Definitions	x:A  B(x), x:A. B(x), x:A. B(x), e  X, t  T, b, Type, x. t(x), Id, Knd, t.2, kind(e), s = t, P & Q, x.A(x), t.1, loc(e), E, {x:A| B(x)} , x:AB(x), P  Q, P  Q, X is finite, type List, (x  l), AbsInterface(A), ES, f(a), , a = b, mapfilter(f;P;L), map(f;as), <a, b>, , S  T, l[i], ||as||, False, A, A  B, , , A c B, a < b, #$n, Void, P  Q, if b then t else f fi
Lemmas	assert-eq-id, member-mapfilter, and functionality wrt iff, member map, l member wf, select wf, mapfilter wf, finite-type-iff-list, Id wf, Knd wf, es-E wf, es-loc wf, pi1 wf, es-kind wf, pi2 wf, assert wf, es-is-interface wf